The presented invention relates generally to the use of hardware description languages to specify circuit logic design in a format that is acceptable to logic synthesis tools, and, more particularly, to a system and method for unifying the specification of design constraints and properties using a hardware description language (HDL) independent assertion format.
Hardware logic design is preferably tested prior to manufacture. The objective of design verification is to ensure that a design""s implementation satisfies the requirements of its specification. Design analysis enables the design engineer to uncover errors at a point of the design phase where they will still be relatively inexpensive to fix. In order to make verification and analysis of logic design economically feasible, it is desirable to dramatically reduce the cost of design specification and automate the analysis process.
Design engineers traditionally verify their design using a black-box testing approach in which the engineer will first create a model of the design written in a hardware description language (HDL), such as Verilog [IEEE 1364-1995] or VHDL [IEEE 1076-1993]; the design model is often referred to as the device-under-test (DUT) in a verification process. The engineer will then create a model of the design environment, referred to as a testbench, which will include or instantiate a copy of the DUT. The testbench is responsible for driving stimulus, i.e., logical one and zero values, into the DUT. In addition, the testbench provides the means for observing and validating the output response values from the DUT. The specification defines the values or sequences of values permitted by the DUT.
One problem with using a black-box testing approach to validate proper design behavior is that it is limited to observing output ports of the DUT. The DUT might exhibit improper internal behavior, such as if a state machine violates its one-hot property (meaning that only one bit is actively high after a reset), but still have proper output response values because the design error is not directly observable on the output ports. This might be due to the current set of input stimulus, when applied to the DUT, impeding the internal problem from propagating to an output port. Given a different set of input stimulus the internal error might be observable. Hence, validating all internal properties of a design using black-box testing techniques is often impractical, particularly as design size increases.
White-box testing is an alternative technique for validating properties of a design. This technique creates test monitors and checkers on internal points within the DUT, resulting in an increase in observable behavior during testing. The previous assertion that a state machine within the DUT is always one-hot can be validated by adding an internal checker to directly monitor each register bit of the state machine. Thus, if the one-hot property is violated, the error is instantly isolated to the problem. This overcomes the problem of black-box testing possibly missing an internal error (for a given input stimuli) by only observing DUT output responses.
There currently exist several types of design verification and analysis tools for validating correct functional design intent. This set of tools includes logic simulation tools, testbench generation tools, formal verification tools, and semi-formal verification tools. Logic simulation tools are used to model and validate design behavior responses for a given set of input stimuli or test vectors; of course, the results obtained using logic simulation tools are only as good as the quality of the set of input stimuli used. Testbench generation tools are used to generate design input stimuli and specify events and assertions for validation in their proprietary languages. So-called formal tools include state-space exploration, static property checker and model checker tools that validate user-specified properties using static and formal techniques without test vectors. Formal tools are heavily proof driven and mathematical in approach. Semi-formal verification tools, such as amplification tools, combine traditional simulation techniques with formal state-space exploration and model checking techniques. The mathematical proofs of the formal tool approach are employed with a limited or bounded search at certain times during the verification process.
One way of specifying a design""s functional intent, expressed by the properties of the design, is to create a set of design assertions representative of the logic design. As an example, consider that a possible design assertion is that a state machine""s encoding is always xe2x80x9cone-hotxe2x80x9d after a reset, meaning that only one bit of a collection of bits is actively high at a time. If the state machine violates the one-hot assertion following a reset, then the logic design is flawed in some way.
In discussing design assertions, it is helpful to understand both verification events and design assertions. A verification event may be defined as an HDL expression, which evaluates to a TRUE value. For example, if the expression (c_ready==1 andand c_reset!=1) evaluates TRUE, then an event has occurred in the verification environment. An assertion is defined as a property of a design, and may be classified as either static or temporal A static assertion is an event that must be TRUE for all time. A temporal assertion has a time relationship of events associated with it, whose correct sequence must be TRUE. For example, a temporal assertion can be viewed as an event-triggered window, bounding a specific property, i.e., an event.
The following examples illustrate aspects of both temporal and static assertions, and combinations thereof. FIG. 1 illustrates an assertion for an invariant property. The property (i.e., event P) in this example is always valid after Event 1 occurs, and continues to be to be TRUE until Event 2 occurs. FIG. 2 illustrates an assertion for a liveness property. The event P, in this example, must eventually be valid after the first event-trigger occurs and before the second event-trigger occurs. In this example, a property of the design is invalid if event P does not occur within the specified event-triggered window.
In addition to static and temporal, an assertion can also be classified as either a constraint or a property, depending upon where the assertion is made. A constraint may be thought of as a range of allowable values. An assertion made on an input port of the design model being verified, referred to as the DUT, is an example of a constraint because it bounds the input stimulus to permissible operating values for that particular input port. The DUT cannot be guaranteed to operate correctly if its input stimulus violates a specified constraint. A property may be thought of as expected behavior in response to defined stimuli (constraints). An assertion made on an output port of a DUT, or an internal point in the design, is an example of a property. For any permissible sequence of input values applied to the DUT, the properties of the design will not be violated if the design is functionally correct. It is noted that the term xe2x80x9cpropertyxe2x80x9d, as used herein, may be used to refer to a property assertion as well as a constraint assertion.
There are several techniques currently available for specifying the assertions, or properties, of a logic design. VHDL [IEEE 1076-1993] provides a language construct for specifying a static invariant assertion. For example:
assert event
report message
severity level
The assert statement can be used as an internal checker during the course of simulation; this is an example of white-box testing.
Unfortunately, VHDL does not provide any constructs for specifying temporal assertion or fiveness properties. In addition, with the exception of logic simulators, commercial verification tools such as property checkers, model checkers and semiformal verification tools will not use the VHDL static assertion construct during verification. In other words, these tools use their own proprietary language to specify a design assertion. Moreover, Verilog [IEEE 1364-1995] does not provide any language constructs for static, temporal, invariance or liveness assertions.
The following examples illustrate different methods currently available for capturing and validating the same design assertion, targeted at: Verilog logic simulation (Example 1), the SMV public-domain model checker [McMillan 1993] (Example 2), general commercial property checking tools (Example 3), and an automaton generation template (Example 4). The design assertion (or property) specified for these examples is that a specific queue in the design cannot underflow when the queue is in a valid state, i.e., when the queue_valid is active high.
For logic simulation, an HDL internal checker can be written to validate the assertion as shown in the following Verilog example:
module QueueSafe (ck, queue_valid, queue_underflow);
always @(posedge ck) begin
if (queue_valid==1xe2x80x2b1) begin
if (!(queue_underflow==1xe2x80x2b0)) begin
xe2x80x83$display (xe2x80x9cERROR: QueueUnderflowxe2x80x9d);
xe2x80x83$finish;
end
end
end
endmodule
During simulation, if the queue_underflow signal is ever activated when the queue is in a valid state, the QueueSafe module will display an error and stop simulation.
Alternatively, the assertion could be specified as an embedded temporal property language, such as CTL, which stands for Computation Tree Logic [Clarke and Emerson 1981], in the HDL as a meta-comment, and then used by a public domain model checker such as symbolic model verifier (SMV) [McMillan 1993]. For example:
//assert: QueueSafe: AG((queue_valid==1))= greater than (queue_underflow!=1)
This CTL Verilog meta-comment expresses the same assertion or property of the design as is modeled with the Verilog QueueSafe module in Example 1.
Many commercial tools have developed their own HDL assertion language, generally using meta-comments similar to the following convention:
//{vendor_name}:{vendor proprietary assertion language}
Thus, multiple meta-comments would be required when using multiple vendor verification tools.
U.S. Pat. No. 5,966,516, entitled, xe2x80x9cApparatus for defining properties in finitestate machines,xe2x80x9d describes a method for specifying system properties in a finite set of templates, which can generate computer-executable code (e.g., automata) intended to test the behavioral attributes of the system. A shortcoming of this approach is that it does not capture the properties of the design directly within the HDL. In addition, this method does not solve the problem of re-targeting the assertions (constraints and properties) to a diverse set of verification tools; each tool must use its own proprietary assertion specification languages.
As illustrated in Examples 1-4, the lack of formal language constructs for assertion specification in today""s HDLs has caused a myriad of proprietary, commercial, tool-specific verification assertion languages to emerge. In order to express the same property of a design as an assertion for many different verification processes and tools, many different representations of the assertion are required. It is clear that there exists an unmet need in the art to be able to represent an assertion of a logic design model in a standardized way, regardless of what type of verification processes and/or tools are used.
The present invention relates generally to hardware description languages to specify circuit logic design in a format that is acceptable to logic synthesis tools and methods therefore. Objects, advantages and features of the invention will become apparent to those skilled in the art upon consideration of the following detailed description of the invention.
In accordance with an exemplary embodiment, a method consistent with the invention of specifying hardware description language assertions targeting a diverse set of verification tools to provide verification of a logic design by the set of verification tools includes the following: specifying properties and constraints of the logic design in an input HDL code that defines a process for verifying the logic design; defining a plurality of assertion macros, representative of the properties and constraints of the logic design and called by a plurality of corresponding assertion macro calls within the input HDL code, in a plurality of macro definitions; a macro processor reading the input HDL code; in response to reading an assertion macro call in the input HDL code, the macro processor accessing a macro definition of the assertion macro corresponding to the assertion macro call, using the macro definition as a template to automatically generate a replacement HDL code, substituting the replacement HDL code for the assertion macro call in the input HDL code, and automatically placing a tool-specific HDL code definition section of the macro definition within a corresponding tool-specific modules library; and repeating this approach for each assertion macro call in the input HDL code to yield a tool-independent output HDL code capable of being executed by any tool of a plurality of tools anticipated to be available to verify the logic design. A similar method may be carried out for a single assertion macro.
The above, exemplary method, as well as other methods of the invention, may be embodied in a computer readable storage medium contains executable instructions which, when executed in a processing system, causes the system to specify hardware description language assertions targeting a diverse set of verification tools to provide verification of a logic design by the set of verification tools.
A system suitable for specifying hardware description language assertions targeting a diverse set of verification tools to provide verification of a logic design by the set of verification tools, consistent with embodiments of the invention, includes: a macro processor, a plurality of tool-specific module libraries, and a macro definition library. The macro processor is provided with an input hardware description language (HDL) code which defines a process for verifying the logic design and which contains a plurality of assertion macro calls corresponding to a plurality of assertion macros that are representative of properties and constraints of the logic design. The macro definition library stores a plurality of macro definitions that define the plurality of assertion macros. The plurality of tool-specific module libraries correspond to a plurality of tools anticipated to be available to verify the logic design. In response to reading an assertion macro call of the plurality of assertions macro calls in the input HDL code, the macro processor accesses a macro definition of a corresponding assertion macro of the plurality of assertion macros from the macro definition library and uses the macro definition as a template to automatically generate a replacement HDL code and substitute the replace HDL code for the assertion macro call and to automatically place a tool-specific HDL code definition section of the macro definition within a corresponding tool-specific modules library of the plurality of tool-specific modules libraries.
Many variations, equivalents and permutations of these illustrative exemplary embodiments of the invention will occur to those skilled in the art upon consideration of the description that follows. The particular examples above should not be considered to define the scope of the invention.